home *** CD-ROM | disk | FTP | other *** search
/ Language/OS - Multiplatform Resource Library / LANGUAGE OS.iso / quintus / quintus0.lha / work / spc_2.06.2 < prev    next >
Text File  |  1992-04-03  |  14KB  |  449 lines
  1. %%% SMALL PROOF CHECK
  2. %%% version 2.04.0 (based on spc_18.9)
  3. %%%   changed spc time bound factor from 2 to 3
  4. %%% version 2.04.5
  5. %%%   added small_proof_nucleus_bound
  6. %%% version 2.05.3
  7. %%%   added support for Quintus Prolog
  8. %%% version 2.06.2
  9. %%%   fixed Quintus Prolog existence error in small proof checker
  10. %%%   added time bound for simple small proof checking
  11. %%%   terminated small proof check if time limit exceeded
  12. %%% 
  13. %%% Find if a clause can unify with unit clauses directly or indirectly.
  14. %%% The idea is as follows:
  15. %%%    Take a clause C = [L1,L2,...,Ln]. Search a clause D = [M1,M2,...,Mm]
  16. %%%    such that Mi unifies with L1 and the remaining literals of D
  17. %%%    unifies with unit clauses. Similarly for L2,..., and Ln.
  18. %%%    If we can find such a C, then the set of clauses is unsatisfiable.
  19. %%% Two options:
  20. %%%    Use input clauses as nuclei, i.e. C.
  21. %%%    Use all clauses as nuclei.
  22. %%% Instance deletion:
  23. %%%    We only consider those clauses which is not an instance of other
  24. %%%    clauses.
  25. %%% Time control:
  26. %%%    Use the time spent in the last hyper-matching as time-limit for
  27. %%%    the small proof checking.
  28. %%% Replacement consideration:
  29. %%%     If replacement is specified, we should use all clauses as nuclei.
  30. %%% Ground literals are matched first.
  31. %%% Change small proof size definition.
  32. %%%    If a literal L in a nucleus is ground, don't count size for the 
  33. %%%    electron of L. 
  34. %%%    Otherwise, increase size count by the length of the electron - 1.
  35. %%%    This definition is concerned with the number of backtracking.
  36. %%% We always check for unit electrons first.
  37. %%% Ordering clauses.
  38. %%%    We order clauses by the number of non-ground literals.
  39. %%% 
  40.  
  41.      spc :- not(not(spc_fail)).
  42.  
  43.      spc_fail :-
  44.     small_proof_check,
  45.     cputime(TT1),
  46.     spc(Result),
  47.     cputime(TT4),
  48.     TT5 is TT4 - TT1,
  49.     write_line(5,'Small proof checking(s): ',TT5),
  50.     !,
  51.     Result == 1.
  52.      spc_fail :-
  53.           fail.
  54.     
  55. %%% If no unit clauses, then done.
  56. %%% Otherwise, find non-instant clauses.
  57.      spc(R) :-
  58.     sent_C(cl(_,_,by([_],_,_,_,_),_,_,_,_,_,_)),
  59.     not(not(find_non_instances)),
  60.     spc_1(R),
  61.     not(not(spc_clear)).
  62.      spc(0).
  63.  
  64.      spc_clear :-
  65.     abolish(spc_stop,0),
  66.     abolish(cps_A,5),
  67.     abolish(cps_I,6),
  68.     abolish(cps_O,5),
  69.     abolish(cps_U,5),
  70.     abolish(cps_V,5).
  71.  
  72. %%% If succeeds, print out the instance and its electrons.
  73.      spc_1(1) :-
  74.     spc_1_1(Cnn,Cn1,Electrons),
  75.     print_out_sp(Cnn,Cn1,Electrons).
  76.      spc_1(0).
  77.  
  78. %%% Obtain small proof size bound.
  79. %%% Obtain time limit.
  80. %%% Set intial time.
  81.      spc_1_1(Cnn,Cn1,Electrons) :-
  82.     clause_largest_length(L),
  83.     LL is L - 1,
  84.     get_spsb(LL,B),
  85.     get_last_hypermatch_time(Tl),
  86.     not(not(initialize_spc_time)), !,
  87.     spc_2(B,LL,Tl,Cnn,Cn1,Electrons,Size), 
  88.     assert(sp_size(Size)).
  89.  
  90. %%% Obtain small proof size bound.
  91.      get_spsb(LL,D) :-
  92.         small_proof_size_bound(N),
  93.         X is LL*(LL+1),
  94.         minimum(N,X,D).
  95.      get_spsb(_,0).
  96.  
  97. %%% Obtain time limit.
  98. %%% 10 seconds for the 0th round.
  99.      get_last_hypermatch_time(T) :-
  100.     round_no(X1),
  101.     get_last_hypermatch_time(X1,T4),
  102.     get_spc_time_factor(P),
  103.     T is P * T4.
  104.      get_last_hypermatch_time(0,10) :- !.
  105.      get_last_hypermatch_time(_,T3) :-
  106.     last_hypermatch_time(T3).
  107.  
  108. %%% Obtain time factor.
  109.      get_spc_time_factor(P) :-
  110.     spc_time_factor(P).
  111.      get_spc_time_factor(3).
  112.  
  113. %%% Set intial time.
  114.      initialize_spc_time :-
  115.     abolish(start_spc_time,1),
  116.     cputime(T),
  117.     assert(start_spc_time(T)).
  118.  
  119. %%% Find a contradiction with unit electrons first.
  120.      spc_2(_,_,Tl,Cnn,Cn1,Es,0) :-
  121.     spc_2_U(Tl,Cnn,Cn1,Es).
  122. %%% Run starting from size 0 to the small proof size bound.
  123.      spc_2(B,LL,Tl,Cnn,Cn1,Es,Size) :-
  124.     \+ simple_small_proof_check,
  125.     spc_2_1(0,B,LL,Tl,Cnn,Cn1,Es,Size).
  126.  
  127. %%% A small proof check succeeds.
  128.      spc_2_1(B1,B2,LL,Tl,Cnn,Cn1,Es,B1) :-
  129.     spc_round(B1,LL,Tl,Cnn,Cn1,Es), !.
  130. %%% If clauses are deleted, then stop.
  131. %%% Otherwise do next round.
  132.      spc_2_1(B1,B2,LL,Tl,Cnn,Cn1,Es,Size) :-
  133.     not(spc_stop),
  134.         not(is_time_overflow),
  135.     BB is B1 + 1,
  136.     !, BB =< B2,
  137.     !, spc_2_1(BB,B2,LL,Tl,Cnn,Cn1,Es,Size).
  138.  
  139. %%% Chceck for unit electrons.
  140.      spc_2_U(Tl,Cnn,Cn1,Es) :-
  141.     spc_nucleus_U(Cnn,Cn1,Ws1),
  142.     check_spc_nucleus_bound(Cn1),
  143.     negate_clause(Cn1,NCn1),
  144.     spc_2_U_clause(NCn1,Ws1,Es,Tl).
  145.  
  146. %%% Contradicting a clause.
  147.      spc_2_U_clause([L1|Ls1],Ws1,[[L2]|Es],Tl) :-
  148.     spc_lit_reorder_2(Ws1,[L1|Ls1],W2,Ws2,L2,Ls2),
  149.     !, spc_unify_unit(L2,Tl),
  150.     !, spc_2_U_clause(Ls2,Ws2,Es,Tl).
  151.      spc_2_U_clause([L1|Ls1],[W1|Ws1],[[L1]|Es],Tl) :-
  152.     spc_unify_unit(L1,Tl),
  153.     w1_w2(Ws1,Ws2),
  154.     spc_2_U_clause(Ls1,Ws2,Es,Tl).
  155.      spc_2_U_clause([],[],[],_).
  156.  
  157. %%% Pick nucleus for unit electrons.
  158. %%% At round 0, we have to consider unit clauses as nucleus,
  159. %%% otherwise we will get trouble with the following set:
  160. %%% [p(a,X)].
  161. %%% [not p(Y,b)].
  162.      spc_nucleus_U([Lnn],[Ln1],Ws1) :-
  163.     not(spc_stop),
  164.         not(is_time_overflow),
  165.     spc_unit_nucleus_condition,
  166.         clause(cps_U(_,Ln1,V11,V11,Ws1),true,Ref1),
  167.     clause(cps_U(_,Lnn,Vnn,Vnn,_),true,Ref1).
  168.      spc_nucleus_U(Cnn,Cn1,Ws1) :-
  169.     spc_nucleus(Cnn,_,Cn1,Ws1).
  170.  
  171.      spc_unit_nucleus_condition :-
  172.         round_no(0),
  173.     !, session_no(1),
  174.     !, \+ tried_round0(1).
  175.  
  176. %%% Do not consider unit clauses as nuclei.
  177. %%% If small_proof_check_all.
  178.      spc_nucleus(Cnn,CV1,Cn1,Ws1) :-
  179.         small_proof_check_all, !,
  180.         clause(cps_A(CV1,Cn1,V11,V11,Ws1),true,Ref1),
  181.     not(spc_stop),
  182.         not(is_time_overflow),
  183.     clause(cps_A(_,Cnn,Vnn,Vnn,_),true,Ref1).
  184. %%% If not small_proof_check_all.
  185. %%% If replacement is specified, we should use all clauses as nuclei.
  186.      spc_nucleus(Cnn,CV1,Cn1,Ws1) :-
  187.         replacement, !,
  188.         clause(cps_A(CV1,Cn1,V11,V11,Ws1),true,Ref1),
  189.     not(spc_stop),
  190.         not(is_time_overflow),
  191.     clause(cps_A(_,Cnn,Vnn,Vnn,_),true,Ref1).
  192. %%% otherwise, we only use input clauses as nuclei.
  193.      spc_nucleus(Cnn,CV1,Cn1,Ws1) :-
  194.         clause(cps_O(CV1,Cn1,V11,V11,Ws1),true,Ref1),
  195.     clause(cps_O(_,Cnn,Vnn,Vnn,_),true,Ref1).
  196.  
  197. %%% Unify with a unit clause.
  198.      spc_unify_unit(L1,Tl) :-
  199.     not(not(spc_time_underflow(Tl))),
  200.     cps_U(_,L1,V11,V12,_),
  201.     unify_lists(V11,V12),
  202.     not(not(spc_time_underflow(Tl))).
  203.  
  204. %%% Get a nucleus.
  205. %%% Check if we have to run this nucleus to avoid redundancy.
  206. %%% Run this nucleus.
  207.      spc_round(0,LL,Tl,Cnn,Cn1,Es) :-
  208.     !, spc_nucleus(Cnn,0,Cn1,Ws1),
  209.     check_spc_nucleus_bound(Cn1),
  210.     negate_clause(Cn1,NCn1),
  211.     spc_clause(NCn1,Ws1,0,LL,0,Tl,1,Es).
  212.      spc_round(B1,LL,Tl,Cnn,Cn1,Es) :-
  213.     spc_nucleus(Cnn,CV1,Cn1,Ws1),
  214.     CV1 \== 0,
  215.     check_spc_nucleus_bound(Cn1),
  216.     negate_clause(Cn1,NCn1),
  217.     spc_clause(NCn1,Ws1,CV1,LL,B1,Tl,1,Es).
  218.  
  219. %%% Check to avoid redundancy.
  220.      spc_check_bound(CV1,LL,B1) :-
  221.     X is CV1 * LL,
  222.     !, X >= B1.
  223.  
  224. %%% Check one literal at a time.
  225.      spc_clause([L1|Ls1],Ws1,CV1,LL,B1,Tl,F1,[E|Es]) :-
  226.     spc_check_bound(CV1,LL,B1),
  227.     Bl is B1 + 1,
  228.     !, spc_literal([L1|Ls1],Ws1,CV1,B1,Bl,Tl,F1,Ls2,Ws2,CV2,F2,E,B2),
  229.         spc_clause(Ls2,Ws2,CV2,LL,B2,Tl,F2,Es).
  230.      spc_clause([],_,_,_,_,_,_,[]).
  231.  
  232. %%% If the literal is the last literal, then we treat it as ground since
  233. %%%    if it succeeds, we have found a contradiction. So no backtracking.
  234.      spc_literal([L1],_,_,_,Bl,Tl,F1,[],_,_,_,E,_) :-
  235.     !, spc_literal_last(Bl,F1,L1,Tl,E).
  236. %%% If the literal is ground.
  237.      spc_literal(Ls1,Ws1,CV1,B1,_,Tl,F1,Ls2,Ws2,CV1,F2,E,B1) :-
  238.     spc_lit_reorder_2(Ws1,Ls1,_,Ws2,L2,Ls2),
  239.         !, spc_literal_gall(F1,L2,Tl,F2,E), !.
  240. %%% If the literal is not ground.
  241. %%% If the literal is next to the last one, we don't update W.
  242.      spc_literal([L1|[Ls1]],_,CV1,B1,Bl,Tl,F1,[Ls1],_,CV2,F2,E,B2) :-
  243.     !, spc_literal_vall(B1,Bl,F1,L1,Tl,F2,E,B2),
  244.     CV2 is CV1 - 1.
  245. %%% If the literal is not ground.
  246.      spc_literal([L1|Ls1],[_|Ws1],CV1,B1,Bl,Tl,F1,Ls1,Ws2,CV2,F2,E,B2) :-
  247.         spc_literal_vall(B1,Bl,F1,L1,Tl,F2,E,B2),
  248.     w1_w2(Ws1,Ws2),
  249.     CV2 is CV1 - 1.
  250.  
  251. %%% If the literal is the last literal in a nucleus.
  252.      spc_literal_last(1,1,_,_,_) :- !, fail.
  253.      spc_literal_last(1,_,L1,Tl,[L1]) :-
  254.     spc_unify_unit(L1,Tl).
  255.      spc_literal_last(B1,_,L1,Tl,E) :-
  256.     spc_nonunit_electron_N(B1,L1,Tl,E).
  257.  
  258. %%% Consider a non-unit electron with length B1.
  259.      spc_nonunit_electron_N(B1,L1,Tl,Cn2) :-
  260.     cps_V(B1,Cn2,V21,V22,Ws2),
  261.     spc_unify_electron(L1,Tl,Cn2,V21,V22,Ws2).
  262.  
  263. %%% Unify an electron.
  264.      spc_unify_electron(L1,Tl,Cn2,V21,V22,Ws2) :-
  265.     not(not(spc_time_underflow(Tl))),
  266.     oneliteral_match(Cn2,V21,V22,Ws2,L1,Tl),
  267.     not(not(spc_time_underflow(Tl))).
  268.  
  269. %%% Consider an electron for a ground literal of a nucleus.
  270.      spc_literal_gall(F1,L1,Tl,F1,[L1]) :-
  271.     spc_unify_unit(L1,Tl).
  272.      spc_literal_gall(_,L1,Tl,2,E) :-
  273.     spc_nonunit_electron_g(L1,Tl,E).
  274.  
  275. %%% Consider a non-unit electron for a ground literal of a nucleus.
  276.      spc_nonunit_electron_g(L1,Tl,Cn2) :-
  277.     cps_V(_,Cn2,V21,V22,Ws2),
  278.     spc_unify_electron(L1,Tl,Cn2,V21,V22,Ws2).
  279.  
  280. %%% Consider an electron for a non-ground literal of a nucleus.
  281.      spc_literal_vall(B1,_,F1,L1,Tl,F1,[L1],B1) :-
  282.     spc_unify_unit(L1,Tl).
  283.      spc_literal_vall(B1,Bl,_,L1,Tl,2,E,B2) :-
  284.     spc_nonunit_electron_v(B1,Bl,L1,Tl,E,B2).
  285.  
  286. %%% Consider a non-unit electron for a non-ground literal of a nucleus.
  287.      spc_nonunit_electron_v(B1,Bl,L1,Tl,Cn2,B2) :-
  288.     cps_V(CV2,Cn2,V21,V22,Ws2),
  289.     Bl >= CV2,
  290.     spc_unify_electron(L1,Tl,Cn2,V21,V22,Ws2),
  291.     B2 is B1 - CV2 + 1.
  292.     
  293. %%% Unifies one literal, and matches the left with unit clauses.
  294.      oneliteral_match(Cn2,V21,V22,Ws2,L1,Tl) :-
  295.     mate_and_rest(Cn2,V21,V22,Ws2,L1,Ls3,W1,Ws3),
  296.     negate_clause(Ls3,NLs3),
  297.     spc_w1_w2(W1,Ws3,Ws4),
  298.         spc_unify_units(NLs3,Ws4,Tl).
  299.  
  300.      mate_and_rest([L1|Ls3],V21,V22,[W1|Ws2],L1,Ls3,W1,Ws2) :-
  301.         unify_lists(V21,V22).
  302.      mate_and_rest([L2|Ls2],V21,V22,[W2|Ws2],L1,[L2|Ls3],W1,[W2|Ws3]) :-
  303.         mate_and_rest(Ls2,V21,V22,Ws2,L1,Ls3,W1,Ws3).
  304.  
  305. %%% If W1 is var, do nothing.
  306.      spc_w1_w2(W1,Ws3,Ws3) :-
  307.     var(W1), !.
  308.      spc_w1_w2(_,Ws3,Ws4) :-
  309.     w1_w2(Ws3,Ws4), !.
  310.  
  311. %%% Unifies with unit clauses.
  312.      spc_unify_units([L1|Ls1],Ws1,Tl) :-
  313.     spc_lit_reorder_2(Ws1,[L1|Ls1],_,Ws2,L2,Ls2),
  314.     !, spc_unify_unit(L2,Tl),
  315.     !, spc_unify_units(Ls2,Ws2,Tl).
  316.      spc_unify_units([L1|Ls1],[_|Ws1],Tl) :-
  317.     spc_unify_unit(L1,Tl),
  318.     w1_w2(Ws1,Ws2),
  319.     spc_unify_units(Ls1,Ws2,Tl).
  320.      spc_unify_units([],_,_).
  321.  
  322. %%% Check time overflow.
  323.      spc_time_underflow(Tl) :-
  324.         spc_time_underflow_1(Tl), !.
  325.      spc_time_underflow(_) :-
  326.         assert_once(spc_stop), !, fail.
  327.  
  328.      spc_time_underflow_1(Tl) :-
  329.     cputime(T1),
  330.     start_spc_time(T2),
  331.     T3 is T1 - T2, !,
  332.     T3 =< Tl.
  333.  
  334. %%% Find all clauses which is not an instance of other clauses.
  335. %%% The non-instance clauses are asserted into database in increasing size
  336. %%% of literals.
  337.  
  338.      find_non_instances :-
  339.         find_non_instances_input,
  340.         find_non_instances_hm,
  341.         order_clause, !.
  342.  
  343.      find_non_instances_input :-
  344.         sent_C(cl(_,CN1,by(Cn1,V11,V12,V1,W1),1,_,_,_,_,_)),
  345.         check_instance(1,CN1,Cn1,V11,V12,V1,W1),
  346.         fail.
  347.      find_non_instances_input.
  348.        
  349.      find_non_instances_hm :-
  350.         sent_C(cl(_,CN1,by(Cn1,V11,V12,V1,W1),0,_,_,_,_,_)),
  351.         check_instance(0,CN1,Cn1,V11,V12,V1,W1),
  352.         fail.
  353.      find_non_instances_hm.
  354.        
  355.      check_instance(T,CN1,[X],V11,V12,V1,W1) :-
  356.         asserta(cps_I(T,CN1,[X],V11,V12,W1)), !.
  357.      check_instance(T,CN1,Cn1,V11,V12,V1,W1) :-
  358.         check_instance_1(T,CN1,Cn1,V11,V12,V1,W1), !.
  359.  
  360. %%% We assume that input clauses are not instances of other clauses.
  361.      check_instance_1(1,CN1,Cn1,V11,V12,_,W1) :-
  362.         asserta(cps_I(1,CN1,Cn1,V11,V12,W1)), !.
  363.      check_instance_1(T,CN1,Cn1,V11,V12,V1,W1) :-
  364.         \+ clause_instance(CN1,Cn1,V11,V12,V1),
  365.         asserta(cps_I(T,CN1,Cn1,V11,V12,W1)), !.
  366.      check_instance_1(_,_,_,_,_,_,_).
  367.        
  368.      clause_instance(CN1,Cn1,V11,V11,V1) :-
  369.         const_list(V1), !,
  370.         cps_I(_,CN1,Cn1,V21,V21,_).
  371.  
  372. %%% Order the clauses by the number of literals.
  373.      order_clause :-
  374.     order_clause_1(0).
  375.      order_clause :-
  376.     order_clause_2.
  377.      order_clause.
  378.  
  379.      order_clause_1(N) :-
  380.     cps_I(_,_,_,_,_,_),
  381.     order_clause_1_1(N),
  382.     NN is N + 1,
  383.     !, order_clause_1(NN).
  384.  
  385. %%% Pick up clauses with N non-ground literals.
  386.      order_clause_1_1(N) :-
  387.     retract(cps_I(T,N,Cn1,V11,V12,W1)),
  388.     assertz(cps_A(N,Cn1,V11,V12,W1)),
  389.     assert_cps_O(Cn1,T,N,V11,V12,W1),
  390.     fail.
  391.      order_clause_1_1(_).
  392.  
  393. %%% We put aside input clauses.
  394. %%% We don't assert unit clauses.
  395.      assert_cps_O([_],_,_,_,_,_) :- !, fail.
  396.      assert_cps_O(Cn1,1,N,V11,V12,W1) :-
  397.     assertz(cps_O(N,Cn1,V11,V12,W1)), !.
  398.  
  399. %%% Retract unit clauses.
  400.      order_clause_2 :-
  401.     order_clause_2_U.
  402. %%% Separate all non-ground literals clauses.
  403.      order_clause_2 :-
  404.     order_clause_2_V.
  405.  
  406. %%% Retract unit clauses.
  407.      order_clause_2_U :-
  408.     retract(cps_A(N,[X],V11,V12,W1)),
  409.     assertz(cps_U(N,X,V11,V12,W1)),
  410.     fail.
  411.  
  412. %%% Separate all non-ground literals clauses.
  413.      order_clause_2_V :-
  414.     cps_A(N,Cn1,V11,V12,W1),
  415.     length(Cn1,N),
  416.     assertz(cps_V(N,Cn1,V11,V12,W1)),  
  417.     fail.
  418.     
  419. %%% Print out nucleus, instance and electrons.
  420.      print_out_sp(Cnn,Cn1,Electrons) :-
  421.         write_line(10,'Small proof found at nucleus:'),
  422.         vars_tail(Cnn,Vn),
  423.         print_clause_2(10,Cnn,Vn),
  424.         vars_tail(Cn1,V1),
  425.         write_line(10,'The instance is:'),
  426.         print_clause_2(10,Cn1,V1),
  427.         write_line(10,'The electrons are:'),
  428.         init_num,
  429.         print_electrons(Electrons).
  430.  
  431. %%% Print out electrons.
  432.      print_electrons([E|Es]) :-
  433.         vars_tail(E,V),
  434.         next_num(N),
  435.         write_numberedline_head(10,N,'.'),
  436.         print_clause_2(2,E,V), !,
  437.         print_electrons(Es).
  438.      print_electrons([]).
  439.  
  440.      spc_lit_reorder_2(W1,Ls,W11,Ws1,L1,Ls1) :-
  441.     spc_literal_reordering,
  442.     !, sep_gr_lit_2(W1,Ls,W11,Ws1,L1,Ls1).
  443.  
  444. %%% Check small proof nucleus bound.
  445.      check_spc_nucleus_bound(C) :-
  446.     length(C,N1),
  447.     small_proof_nucleus_bound(N2),
  448.     N1=<N2,
  449.     !.